\section{Resolution}

\begin{enumerate}[(a)]
	\item
		\begin{enumerate}[i)]
			%i
			\item $ (\forall x P(x) \rightarrow \forall x Q(x)) \vee \forall x (P(x) \rightarrow Q(y)) $
			
			\begin{align*}
				& \equiv ( \neg \forall x P(x) \vee \forall x Q(x)) \vee \forall x (\neg P(x) \vee Q(y)) \\
				& \equiv ( \exists x \neg P(x) \vee \forall x Q(x)) \vee \forall x (\neg P(x) \vee Q(y)) \\
				& \equiv \exists x ( \neg P(x) \vee \forall a Q(a)) \vee \forall x (\neg P(x) \vee Q(y)) \\
				& \equiv \exists x \forall a ( \neg P(x) \vee  Q(a)) \vee \forall x (\neg P(x) \vee Q(y)) \\
				& \equiv \exists x (\forall a ( \neg P(x) \vee  Q(a)) \vee \forall x (\neg P(x) \vee Q(y)) )\\
				& \equiv \exists x \forall a  (( \neg P(x) \vee  Q(a)) \vee \forall x (\neg P(x) \vee Q(y)) )\\
				& \equiv \exists x \forall a  \forall b (( \neg P(x) \vee  Q(a)) \vee  (\neg P(b) \vee Q(y)) )\\
			\end{align*}

			
			%ii
			\item $ \forall x (P(x,y) \rightarrow Q(x)) \rightarrow \exists y R(a,f(x,y)) $
			
			\begin{align*}
				& \equiv \forall x (P(x,y) \rightarrow Q(x)) \rightarrow \exists y R(a,f(x,y)) \\
				& \equiv \neg \forall x (\neg P(x,y) \vee Q(x)) \vee \exists y R(a,f(x,y)) \\
				& \equiv  \exists x \neg (\neg P(x,y) \vee Q(x)) \vee \exists y R(a,f(x,y)) \\
				& \equiv  \exists x (\neg (\neg P(x,y) \vee Q(x)) \vee \exists y R(a,f(z,y))) \\
				& \equiv  \exists x \exists y (\neg (\neg P(x,q) \vee Q(x)) \vee  R(a,f(z,y))) \\
			\end{align*}
			
			
			%iii
			\item $ \neg ( \forall x \forall y(P(x,a) \rightarrow \exists x R(x,y,z)) \wedge S(x,y)) $
			
			\begin{align*}
				& \equiv \neg ( \forall x \forall y(\neg P(x,a) \vee \exists x R(x,y,z)) \wedge S(x,y)) \\
				& \equiv \exists x \exists y \neg (\neg P(x,a) \vee \exists x R(x,y,z)) \wedge S(x,y)) \\
				& \equiv \exists x \exists y ( P(x,a) \wedge \neg (\exists x R(x,y,z))) \wedge S(x,y)) \\
				& \equiv \exists x \exists y ( P(x,a) \wedge  \forall x \neg R(x,y,z)) \wedge S(x,y)) \\
				& \equiv \exists x \exists y (( P(x,a) \wedge  \forall x \neg R(x,y,z)) \wedge S(q,p))) \\
				& \equiv \exists x \exists y (\forall r ( P(x,a) \wedge  \neg R(r,y,z)) \wedge S(q,p))) \\
				& \equiv \exists x \exists y \forall r (( P(x,a) \wedge  \neg R(r,y,z)) \wedge S(q,p))) \\
			\end{align*}
			
			%iv
			\item $ \forall x (J(x) \rightarrow \exists y (M(y) \wedge \exists y H(x,y))) $
		
			\begin{align*}
				& \equiv \forall x (\neg J(x) \vee \exists y (M(y) \wedge \exists y H(x,y))) \\
				& \equiv \forall x \exists y (\neg J(x) \vee  (M(y) \wedge \exists y H(x,y))) \\
				& \equiv \forall x \exists y (\neg J(x) \vee \exists a (M(y) \wedge  H(x,a))) \\
				& \equiv \forall x \exists y \exists a (\neg J(x) \vee (M(y) \wedge  H(x,a))) \\
			\end{align*}
			
		\end{enumerate}
		
	\item
		\begin{enumerate}[i)]
			%i
			\item $\forall x \exists y R(x,y)$
			
			$F^s = \forall x \ R(x,f(x)) $
			
			%ii
			\item $\forall x(B(x) \rightarrow \exists y (A(y) \wedge R(x,y))) $
			
			\begin{align*}
				& \equiv \forall x(\neg B(x) \vee \exists y (A(y) \wedge R(x,y))) \\
				& \equiv \forall x \exists y (\neg B(x) \vee (A(y) \wedge R(x,y))) \\
				& \equiv \forall x \exists y ( (\neg B(x) \vee A(y)) \wedge (\neg B(x) \vee R(x,y))) \\
				& \equiv \forall x ( (\neg B(x) \vee A(f(x))) \wedge (\neg B(x) \vee R(x,f(x)))) \\
			\end{align*}
			
			
		\end{enumerate}
		
\end{enumerate}